Trait isotope::ctx::eq::TermEqCtxMut [−][src]
pub trait TermEqCtxMut: Debug {}Show methods
fn term_eq_mut(&mut self, left: &Term, right: &Term) -> Option<bool>; fn is_ty_mut(&mut self, ty: &Term) -> Option<bool>; fn root_mut(&mut self, ty: &Term) -> Option<TermId>; fn as_dyn_eq_mut(&mut self) -> &mut dyn TermEqCtxMut; fn cmp_annot(&self) -> bool; fn cmp_param(&self) -> bool; fn cmp_var(&self) -> bool; fn is_struct(&self) -> bool; fn typed_mask(&self) -> L4; fn untyped_mask(&self) -> L4; fn shallow_cons_term_eq(
&mut self,
left: &TermId,
right: &TermId
) -> Option<bool> { ... } fn deep_cons_term_eq(
&mut self,
left: &TermId,
right: &TermId
) -> Option<bool> { ... } fn shallow_cons_is_ty(&mut self, ty: &TermId) -> Option<bool> { ... } fn deep_cons_is_ty(&mut self, ty: &TermId) -> Option<bool> { ... } fn shallow_cons_root(&mut self, ty: &TermId) -> Option<TermId> { ... } fn deep_cons_root(&mut self, ty: &TermId) -> Option<TermId> { ... } fn approx_term_eq_mut(
&mut self,
left: &Term,
right: &Term
) -> Option<Option<bool>> { ... } fn approx_term_eq_code(
&self,
_left: (Code, Form),
_right: (Code, Form)
) -> Option<Option<bool>> { ... } fn cache_eq(&mut self, _left: &TermId, _right: &TermId) { ... } fn shallow_cons_cache_eq(&mut self, left: &TermId, right: &TermId) { ... }
Expand description
A type which may be used as a mutable context for checking isotope
terms for equality
Required methods
Check two terms are equivalent, potentially optimizing the underlying data structure Consing is optional
Check whether this term is equivalent to a type in this context, potentially optimizing the underlying data structure
Get a term’s root form in this context, potentially optimizing the underlying data structure
fn as_dyn_eq_mut(&mut self) -> &mut dyn TermEqCtxMut
[src]
fn as_dyn_eq_mut(&mut self) -> &mut dyn TermEqCtxMut
[src]Get this term as a dynamic typing context
fn typed_mask(&self) -> L4
[src]
fn typed_mask(&self) -> L4
[src]Get the untyped equality mask for this context
fn untyped_mask(&self) -> L4
[src]
fn untyped_mask(&self) -> L4
[src]Get the untyped equality mask for this context
Provided methods
Check two terms are equivalent, potentially optimizing the underlying data structure If this data structure conses, then this will shallow-cons both terms
Check two terms are equivalent, potentially optimizing the underlying data structure If this data structure conses, then this will deep-cons both terms
fn shallow_cons_is_ty(&mut self, ty: &TermId) -> Option<bool>
[src]
fn shallow_cons_is_ty(&mut self, ty: &TermId) -> Option<bool>
[src]Check whether this term is equivalent to a type in this context, potentially optimizing the underlying data structure If this data structure conses, then this will shallow-cons both terms
fn deep_cons_is_ty(&mut self, ty: &TermId) -> Option<bool>
[src]
fn deep_cons_is_ty(&mut self, ty: &TermId) -> Option<bool>
[src]Check whether this term is equivalent to a type in this context, potentially optimizing the underlying data structure If this data structure conses, then this will deep-cons both terms
fn shallow_cons_root(&mut self, ty: &TermId) -> Option<TermId>
[src]
fn shallow_cons_root(&mut self, ty: &TermId) -> Option<TermId>
[src]Get a term’s universe in this context, potentially optimizing the underlying data structure If this data structure conses, then this will shallow-cons both terms
fn deep_cons_root(&mut self, ty: &TermId) -> Option<TermId>
[src]
fn deep_cons_root(&mut self, ty: &TermId) -> Option<TermId>
[src]Get a term’s root form in this context, potentially optimizing the underlying data structure If this data structure conses, then this will deep-cons both terms
Quickly approximate equality between two terms: return None
if unknown
Check whether it is possible for two terms to be equal by code/address alone
Cache two equal terms.
Unlike TermEqEdit
’s make_term_eq
, this is not guaranteed to have an effect.
fn shallow_cons_cache_eq(&mut self, left: &TermId, right: &TermId)
[src]
fn shallow_cons_cache_eq(&mut self, left: &TermId, right: &TermId)
[src]Cache two equal shallow-consed terms.
Unlike TermEqEdit
’s shallow_cons_make_term_eq
, this is not guaranteed to have an effect.